A:Type, eq:EqDecider(A), B:(AType), P:(A), f:x:A fp B(x), x:{a:A| (P(a))} , v:B(x).
(<x, v>  fpf-vals(eq;P;f))  {(x  dom(f)) & v = f(x)} 

latex

Definitions	x:AB(x), P  Q, x:A  B(x), P & Q, P  Q, t  T, x:A. B(x), b, x(s), Type, EqDecider(T), , f(a), x. t(x), a:A fp B(a), {x:A| B(x)} , x.A(x), fpf-vals(eq;P;f), <a, b>, (x  l), s = t, {T}, S  T
Lemmas	l member subtype, l member wf, fpf-vals wf, assert wf, fpf wf, bool wf, deq wf, member-fpf-vals